In our work  [SUNLRLD09], we studied the problem of fair model checking with process counter abstraction. Imagine a bus protocol where a large / unbounded number of processors are contending for bus access. If we do not assume any fairness in the bus arbitration policy, we cannot prove the non-starvation property, that is, bus accesses by processors are eventually granted. In general, fairness constraints are often needed for verification of such liveness properties — ignoring fairness constraints results in unrealistic counterexamples (e.g. where a processor requesting for bus access is persistently ignored by the bus arbiter for example) being reported. These counterexamples are of no interest to the protocol designer. To systematically rule out such unrealistic counterexamples (which never happen in a real implementation), it is important to verify the abstract system produced by our process counter abstraction under fairness.

We also propose a novel technique for model checking parameterized systems under fairness, against Linear Temporal Logic(LTL) formulae. Even without maintaining the process identifiers, our on-the-fly checking algorithm enforces fairness by keeping track of the local states from where actions are enabled / executed within an execution trace. Since parameterized systems contain process types with large number of behaviorally similar processes (whose behavior follows a local finite state machine or FSM), we group the processes based on which state of the local FSM they reside in. Thus, instead of saying “process 1 is in state s, process 2 is in state t and process 3 is in state s” — we simply say “2 processes are in state s and 1 is in state t”. Such an abstraction reduces the state space by exploiting powerful state space symmetry, as often evidenced in real-life concurrent systems such as a caches, memories, mutual exclusion protocols and network protocols. To achieve a finite state abstract system, we can adopt a cutoff number, so that any count greater than the cutoff number is abstracted to w.  This yields a finite state abstract system, model checking which we get a sound but incomplete verification procedure — any linear time Temporal Logic (LTL) property verified in the abstract system holds for all concrete finite-state instances of the system, but not vice-versa. We develop necessary theorems to prove the soundness of our technique, and also present efficient on-the-fly model checking algorithms. Please refer to our paper [SUNLRLD09] for more details such as theorem proving.

Here we take modeling the classic Readers and Writers Problem(Refer to PAT Examples-> Classic Algorithms-> Readers/ Writers Problem) as an example to show how the Process Counter Represetation technique is applied in abstracting a system. This example shows an infinite system of unbounded readers and unbounded writers read and write a shared file, while system allows mutiple read, but forbit read while writing, writing while writing and writing while read actions, i.e. write process should be exclusive.

First, we shall model the individual reader and writer process:

Then with showing a concrete system which has 2 readers and 2 writers, we remark that the abstract transition relation can be constructed without constructing the concrete transition relation, which is essential to avoid state space explosion.

Finally, we can obtain the abstract transition system for a reader/ writer system with unboundedly many processes by applying the aforementioned abstract reansition relation. Here we assume the cutoff number is 1. The abstract system noew has only finitely many states even if there are unbounded number of processes and, therefore, is subject to model checking.

The above three figures show how the process abstract technique applied in our PAT. You can model the reader/writer problem normally, and verify it with our method fast and smoothly.